Funding entity European Research Council Executive Agency
Participated by Institut National de Recherche en Informatique et Automatique INRIA, Centre National de la Recherche Scientifique CNRS, Université Paris Cite
Proof assistants have seen growing adoption among researchers and scientists in recent years, thanks to their ability to efficiently formalise large bodies of mathematics. They have been used to certify major results such as the Scholze liquid tensor challenge and the Kepler conjecture. However, current proof assistants are limited to formal settings and cannot process the flexible, semi-formal language commonly used by mathematicians. The ERC-funded MALINCA project (ERC-2024-SyG - ERC Synergy Grant 101167526) aims to develop a new proof assistant technology that preserves the precision of formal language and mathematical meaning while incorporating greater versatility. It will be designed to understand and represent the dynamic linguistic structures mathematicians use in practice.
Layman's summary: The ERC-funded MALINCA project aims to develop a new proof assistant technology designed to understand and represent the dynamic linguistic structures mathematicians use in practice, preserving the precision of formal language and mathematical meaning while incorporating greater versatility.
MALINCA
